1  /-
  2  Copyright (c) 2018 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  
  6  Definition of splitting fields, and definition of homomorphism into any field that splits
  7  -/
  8  
  9  import ring_theory.unique_factorization_domain
src         └─────────────────────────────────────┘
 10  import data.polynomial ring_theory.principal_ideal_domain
src         └─────────────┘ └────────────────────────────────┘
 11         algebra.euclidean_domain
src         └──────────────────────┘
 12  
 13  local attribute [instance, priority 100000] is_ring_hom.id
 14  
 15  universes u v w
 16  
 17  variables {α : Type u} {β : Type v} {γ : Type w}
 18  
 19  namespace polynomial
 20  
 21  noncomputable theory
 22  open_locale classical
 23  variables [discrete_field α] [discrete_field β] [discrete_field γ]
id              └────────────┘     └────────────┘     └────────────┘
src             └────────────┘     └────────────┘     └────────────┘
typ             └────────────┘     └────────────┘     └────────────┘
 24  open polynomial
 25  
 26  section splits
 27  
 28  variables (i : α → β) [is_ring_hom i]
id                          └─────────┘
src                         └─────────┘
typ                         └─────────┘
doc                         └─────────┘
 29  
 30  /-- a polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1 -/
 31  def splits (f : polynomial α) : Prop :=
id                   └────────┘ 
src                  └────────┘
typ                  └────────┘ 
doc                  └────────┘
 32  f = 0 ∨ ∀ {g : polynomial β}, irreducible g → g ∣ f.map i → degree g = 1
id               └────────┘    └─────────┘      └──┘    └────┘  
src               └────────┘     └─────────┘         └──┘     └────┘   
typ              └────────┘    └─────────┘      └──┘    └────┘  
doc                 └────────┘     └─────────┘          └──┘     └────┘
 33  
 34  @[simp] lemma splits_zero : splits i (0 : polynomial α) := or.inl rfl
id                               └────┘       └────────┘      └────┘ └─┘
src                              └────┘        └────────┘       └────┘ └─┘
typ                              └────┘       └────────┘      └────┘ └─┘
doc    └──┘                      └────┘        └────────┘
 35  
 36  @[simp] lemma splits_C (a : α) : splits i (C a) :=
id                                   └────┘    
src                                   └────┘    
typ                                  └────┘    
doc    └──┘                           └────┘    
 37  if ha : a = 0 then ha.symm ▸ (@C_0 α _).symm ▸ splits_zero i
id                                  └─┘             └─────────┘
src                                 └─┘             └─────────┘
typ                                 └─┘             └─────────┘
 38  else
 39  have hia : i a ≠ 0, from mt ((is_add_group_hom.injective_iff i).1
id                            └┘   └────────────────────────────┘
src                           └┘   └────────────────────────────┘
typ                           └┘   └────────────────────────────┘
 40    (is_ring_hom.injective i) _) ha,
id      └───────────────────┘
src     └───────────────────┘
typ     └───────────────────┘
 41  or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 (classical.not_not.2 (is_unit_iff_degree_eq_zero.2 $
id   └────┘                   └────┘       └───────────────┘    └────────────────────────┘
src  └────┘                   └────┘       └───────────────┘    └────────────────────────┘
typ  └────┘                   └────┘       └───────────────┘    └────────────────────────┘
 42    by have := congr_arg degree hp;
src       └──────┘               
typ       └──────┘               
doc       └──────┘               
txt       └──────┘               
par       └──────┘               
pid       └───┘└─┘               
 43      simp [degree_C hia, @eq_comm (with_bot ℕ) 0,
src      └────┘           └┘                  └────
typ      └────┘           └┘                  └────
doc      └────┘           └┘                  └────
txt      └────┘           └┘                  └────
par      └────┘           └┘                  └────
pid                     └┘                  └────
 44        nat.with_bot.add_eq_zero_iff] at this; clear _fun_match; tautology))
id            └───────────────────────┘
src  ─────┘   └───────────────────────┘└───────┘  └──────────────┘  └───────┘
typ  ─────┘   └───────────────────────┘└───────┘  └──────────────┘  └───────┘
doc  ─────┘                            └───────┘  └──────────────┘  └───────┘
txt  ─────┘                            └───────┘  └──────────────┘  └───────┘
par  ─────┘                            └───────┘  └──────────────┘  └───────┘
pid  ─────┘                            └─────┘       └─────────┘
st            └─────────────────────────────────────────────────────────────┘
 45  
 46  lemma splits_of_degree_eq_one {f : polynomial α} (hf : degree f = 1) : splits i f :=
id                                      └────────┘         └────┘        └────┘  
src                                     └────────┘          └────┘         └────┘
typ                                     └────────┘         └────┘        └────┘  
doc                                     └────────┘          └────┘          └────┘
 47  or.inr $ λ g hg ⟨p, hp⟩,
id   └────┘      └┘ 
src  └────┘
typ  └────┘      └┘ 
 48    by have := congr_arg degree hp;
id                └───────┘ └────┘ └┘
src       └──────┘└───────┘└────┘
typ       └──────┘└───────┘└────┘└┘
doc       └──────┘         └────┘
txt       └──────┘               
par       └──────┘               
pid       └───┘└─┘               
st       └─────────────────────────────
 49    simp [nat.with_bot.add_eq_one_iff, hf, @eq_comm (with_bot ℕ) 1,
id           └─────────────────────────┘  └┘   └─────┘  └──────┘
src    └────┘└─────────────────────────┘└┘  └┘ └─────┘ └──────┘ └────
typ    └────┘└─────────────────────────┘└┘└┘└┘ └─────┘ └──────┘ └────
doc    └────┘                           └┘  └┘                  └────
txt    └────┘                           └┘  └┘                  └────
par    └────┘                           └┘  └┘                  └────
pid                                   └┘  └┘                  └────
st   ──────────────────────────────────────────────────────────────────
 50      mt is_unit_iff_degree_eq_zero.2 hg.1] at this;
id       └┘ └────────────────────────┘   └┘
src  ───┘└┘└────────────────────────┘└─┘  └─────────┘
typ  ───┘└┘└────────────────────────┘└─┘└┘└─────────┘
doc  ───┘                            └─┘  └─────────┘
txt  ───┘                            └─┘  └─────────┘
par  ───┘                            └─┘  └─────────┘
pid  ───┘                            └─┘  └─┘└─────┘
st   ───────────────────────────────────────────────────
 51    clear _fun_match; tauto
src    └──────────────┘  └─────
typ    └──────────────┘  └─────
doc    └──────────────┘  └─────
txt    └──────────────┘  └─────
par    └──────────────┘  └─────
pid         └─────────┘       
st   ──────────────────────────
 52  
src  
typ  
doc  
txt  
par  
pid  
st   
 53  lemma splits_of_degree_le_one {f : polynomial α} (hf : degree f ≤ 1) : splits i f :=
id                                      └────────┘         └────┘        └────┘  
src                                     └────────┘          └────┘         └────┘
typ                                     └────────┘         └────┘        └────┘  
doc                                     └────────┘          └────┘          └────┘
 54  begin
st   └─────
 55    cases h : degree f with n,
id               └────┘ 
src    └────┘ └─┘└────┘ └─────┘
typ    └────┘ └─┘└────┘└─────┘
doc    └────┘ └─┘└────┘ └─────┘
txt    └────┘ └─┘       └─────┘
par    └────┘ └─┘       └─────┘
pid          └─┘       └─────┘
st   ──────────────────────────┘└─
 56    { rw [degree_eq_bot.1 h]; exact splits_zero i },
id           └───────────┘            └─────────┘ 
src      └──┘└───────────┘└─┘   └────┘└─────────┘ 
typ      └──┘└───────────┘└─┘  └────┘└─────────┘
doc      └──┘             └─┘   └────┘            
txt      └──┘             └─┘   └────┘            
par      └──┘             └─┘   └────┘            
pid        └┘             └─┘                    
st   ───┘└───────────────────┘└────────────────────┘└┘
 57    { cases n with n,
id             
src      └────┘ └─────┘
typ      └────┘└─────┘
doc      └────┘ └─────┘
txt      └────┘ └─────┘
par      └────┘ └─────┘
pid            └─────┘
st   ─────────────────┘└─
 58      { rw [eq_C_of_degree_le_zero (trans_rel_right (≤) h (le_refl _))];
id             └────────────────────┘  └─────────────┘      └─────┘
src        └──┘└────────────────────┘ └─────────────┘└─┘  └─────┘└───┘
typ        └──┘└────────────────────┘ └─────────────┘└─┘ └─────┘└───┘
doc        └──┘                                       └─┘         └───┘
txt        └──┘                                       └─┘         └───┘
par        └──┘                                       └─┘         └───┘
pid          └┘                                       └─┘         └───┘
st   ─────┘└────────────────────────────────────────────────────────────┘└─
 59        exact splits_C _ _ },
id               └──────┘
src        └────┘└──────┘└───┘
typ        └────┘└──────┘└───┘
doc        └────┘        └───┘
txt        └────┘        └───┘
par        └────┘        └───┘
pid                     └──┘
st   ────────────────────────┘└┘
 60      { have hn : n = 0,
id                   
src        └────────┘  └┘
typ        └────────┘ └┘
doc        └────────┘  └┘
txt        └────────┘  └┘
par        └────────┘  └┘
pid        └─────┘└─┘  
st   ────────────────────┘└─
 61        { rw h at hf,
id              
src          └─┘ └────┘
typ          └─┘└────┘
doc          └─┘ └────┘
txt          └─┘ └────┘
par          └─┘ └────┘
pid             └────┘
st   ───────┘└────────┘└─
 62          cases n, { refl }, { exact absurd hf dec_trivial } },
id                                     └────┘ └┘ └─────────┘
src          └────┘     └───┘     └────┘└────┘  └─────────┘
typ          └────┘    └───┘     └────┘└────┘└┘└─────────┘
doc          └────┘     └───┘     └────┘        └─────────┘
txt          └────┘     └───┘     └────┘                   
par          └────┘     └───┘     └────┘                   
pid                                                     
st   ──────────────┘└──┘└───┘└┘└─────────────────────────────┘└──┘
 63        exact splits_of_degree_eq_one _ (by rw [h, hn]; refl) } }
id               └─────────────────────┘             └┘
src        └────┘└─────────────────────┘└─┘   └──┘ └┘  └┘└──┘└┘
typ        └────┘└─────────────────────┘└─┘   └──┘└┘└┘└┘└──┘└┘
doc        └────┘                       └─┘   └──┘ └┘  └┘└──┘└┘
txt        └────┘                       └─┘   └──┘ └┘  └┘└──┘└┘
par        └────┘                       └─┘   └──┘ └┘  └┘└──┘└┘
pid                                    └─┘   └───┘ └┘  └──────┘
st   ────────────────────────────────────────┘└────┘└──┘└────┘└┘└───
 64  end
st   ──┘
 65  
 66  lemma splits_mul {f g : polynomial α} (hf : splits i f) (hg : splits i g) : splits i (f * g) :=
id                           └────────┘         └────┘          └────┘      └────┘     
src                          └────────┘          └────┘            └────┘        └────┘      
typ                          └────────┘         └────┘          └────┘      └────┘     
doc                          └────────┘          └────┘            └────┘        └────┘
 67  if h : f * g = 0 then by simp [h]
id   └┘                         
src  └┘                     └────┘ └┘
typ  └┘                   └────┘└┘
doc                           └────┘ └┘
txt                           └────┘ └┘
par                           └────┘ └┘
pid                                
st                           └────────┘
 68  else or.inr $ λ p hp hpf, ((principal_ideal_domain.irreducible_iff_prime.1 hp).2.2 _ _
id        └────┘     └┘ └─┘    └──────────────────────────────────────────┘  └┘  
src       └────┘                 └──────────────────────────────────────────┘      
typ       └────┘     └┘ └─┘    └──────────────────────────────────────────┘  └┘  
 69      (show p ∣ map i f * map i g, by convert hpf; rw polynomial.map_mul)).elim
id               └─┘    └─┘               └─┘     └────────────────┘  └──┘
src               └─┘      └─┘         └──────┘     └─┘└────────────────┘  └──┘
typ              └─┘    └─┘       └──────┘└─┘  └─┘└────────────────┘  └──┘
doc                └─┘       └─┘         └──────┘     └─┘
txt                                      └──────┘     └─┘
par                                      └──────┘     └─┘
pid                                                    
st                                      └───────────────┘└────────────────┘
 70    (hf.resolve_left (λ hf, by simpa [hf] using h) hp)
id      └┘└───────────┘    └┘            └┘          └┘
src       └───────────┘           └─────┘  └──────┘
typ     └┘└───────────┘    └┘     └─────┘└┘└──────┘  └┘
doc                               └─────┘  └──────┘
txt                               └─────┘  └──────┘
par                               └─────┘  └──────┘
pid                                      └────┘
st                               └─────────────────┘
 71    (hg.resolve_left (λ hg, by simpa [hg] using h) hp)
id      └┘└───────────┘    └┘            └┘          └┘
src       └───────────┘           └─────┘  └──────┘
typ     └┘└───────────┘    └┘     └─────┘└┘└──────┘  └┘
doc                               └─────┘  └──────┘
txt                               └─────┘  └──────┘
par                               └─────┘  └──────┘
pid                                      └────┘
st                               └─────────────────┘
 72  
 73  lemma splits_of_splits_mul {f g : polynomial α} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
id                                     └────────┘                      └────┘     
src                                    └────────┘                         └────┘      
typ                                    └────────┘                      └────┘     
doc                                    └────────┘                           └────┘
 74    splits i f ∧ splits i g :=
id     └────┘    └────┘  
src    └────┘      └────┘
typ    └────┘    └────┘  
doc    └────┘       └────┘
 75  ⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
id    └────┘      └─┘ └┘  └─────────────┘  └─┘ └─┘        └─────┘        └───────┘ └┘  └───────────┘
src   └────┘               └─────────────┘               └─┘└─────┘  └────┘└───────┘   └───────────┘└───┘
typ   └────┘      └─┘ └┘  └─────────────┘  └─┘ └─┘     └─┘└─────┘  └────┘└───────┘└┘ └───────────┘└───┘
doc                                                      └─┘         └────┘                         └───┘
txt                                                      └─┘         └────┘                         └───┘
par                                                      └─┘         └────┘                         └───┘
pid                                                                                               └───┘
st                                                      └─────────────────────────────────────────────────┘
 76   or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
id    └────┘      └─┘ └┘  └─────────────┘  └─┘ └─┘        └─────┘        └───────┘ └┘  └──────────┘
src   └────┘               └─────────────┘               └─┘└─────┘  └────┘└───────┘   └──────────┘└───┘
typ   └────┘      └─┘ └┘  └─────────────┘  └─┘ └─┘     └─┘└─────┘  └────┘└───────┘└┘ └──────────┘└───┘
doc                                                      └─┘         └────┘                        └───┘
txt                                                      └─┘         └────┘                        └───┘
par                                                      └─┘         └────┘                        └───┘
pid                                                                                              └───┘
st                                                      └────────────────────────────────────────────────┘
 77  
 78  lemma splits_map_iff (j : β → γ) [is_ring_hom j] {f : polynomial α} :
id                                   └─────────┘        └────────┘ 
src                                    └─────────┘         └────────┘
typ                                  └─────────┘        └────────┘ 
doc                                    └─────────┘         └────────┘
 79    splits j (f.map i) ↔ splits (λ x, j (i x)) f :=
id     └────┘   └──┘    └────┘            
src    └────┘     └──┘     └────┘
typ    └────┘   └──┘    └────┘            
doc    └────┘     └──┘      └────┘
 80  by simp [splits, polynomial.map_map]
id            └────┘  └────────────────┘
src     └────┘└────┘└┘└────────────────┘└─
typ     └────┘└────┘└┘└────────────────┘└─
doc     └────┘└────┘└┘                  └─
txt     └────┘      └┘                  └─
par     └────┘      └┘                  └─
pid               └┘                  
st     └──────────────────────────────────
 81  
src  
typ  
doc  
txt  
par  
pid  
st   
 82  lemma exists_root_of_splits {f : polynomial α} (hs : splits i f) (hf0 : degree f ≠ 0) :
id                                    └────────┘         └────┘           └────┘  
src                                   └────────┘          └────┘             └────┘   
typ                                   └────────┘         └────┘           └────┘  
doc                                   └────────┘          └────┘             └────┘
 83    ∃ x, eval₂ i x f = 0 :=
id       └───┘    
src       └───┘       
typ      └───┘    
doc         └───┘
 84  if hf0 : f = 0 then ⟨37, by simp [hf0]⟩
id   └┘                              └─┘
src  └┘                         └────┘   
typ  └┘                        └────┘└─┘
doc                              └────┘   
txt                              └────┘   
par                              └────┘   
pid                                     
st                              └─────────┘
 85  else
 86    let ⟨g, hg⟩ := is_noetherian_ring.exists_irreducible_factor
id     └─┘     └┘     └──────────────────────────────────────────┘
src                   └──────────────────────────────────────────┘
typ    └─┘     └┘     └──────────────────────────────────────────┘
 87      (show ¬ is_unit (f.map i), from mt is_unit_iff_degree_eq_zero.1 (by rwa degree_map))
id              └─────┘  └──┘         └┘ └────────────────────────┘          └────────┘
src             └─────┘   └──┘          └┘ └────────────────────────┘      └──┘└────────┘
typ             └─────┘  └──┘         └┘ └────────────────────────┘      └──┘└────────┘
doc              └─────┘   └──┘                                              └──┘
txt                                                                          └──┘
par                                                                          └──┘
pid                                                                             
st                                                                          └─────────────┘
 88      (by rw [ne.def, map_eq_zero]; exact hf0) in
id               └────┘  └─────────┘         └─┘
src          └──┘└────┘└┘└─────────┘  └────┘
typ          └──┘└────┘└┘└─────────┘  └────┘└─┘
doc          └──┘      └┘             └────┘
txt          └──┘      └┘             └────┘
par          └──┘      └┘             └────┘
pid            └┘      └┘                  
st          └─────────┘└───────────┘└─────────┘
 89    let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0 hg.1 hg.2) in
id     └─┘           └──────────────────────────┘  └┘└───────────┘ └─┘       
src                   └──────────────────────────┘    └───────────┘           
typ    └─┘           └──────────────────────────┘  └┘└───────────┘ └─┘       
 90    let ⟨i, hi⟩ := hg.2 in
id     └─┘              
src                     
typ    └─┘              
 91    ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _, from hx, zero_mul]⟩
id                  └──────┘  └┘  └──────┘                  └┘  └──────┘
src           └────┘└──────┘└┘  └┘└──────┘└┘    └─┘└───────┘  └┘└──────┘
typ           └────┘└──────┘└┘└┘└┘└──────┘└┘    └─┘└───────┘└┘└┘└──────┘
doc           └────┘        └┘  └┘        └┘    └─┘ └───────┘  └┘        
txt           └────┘        └┘  └┘        └┘    └─┘ └───────┘  └┘        
par           └────┘        └┘  └┘        └┘    └─┘ └───────┘  └┘        
pid             └──┘        └┘  └┘        └┘    └─┘ └───────┘  └┘        
st           └─────────────┘└──┘└────────┘└───────────────────┘└────────┘
 92  
 93  lemma exists_multiset_of_splits {f : polynomial α} : splits i f →
id                                        └────────┘     └────┘  
src                                       └────────┘      └────┘
typ                                       └────────┘     └────┘  
doc                                       └────────┘      └────┘
 94    ∃ (s : multiset β), f.map i = C (i f.leading_coeff) *
id           └──────┘   └──┘      └────────────┘  
src          └──────┘     └──┘         └────────────┘  
typ          └──────┘   └──┘      └────────────┘  
doc           └──────┘      └──┘          └────────────┘
 95    (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
id      └──┘              └────────┘       └──┘
src      └──┘               └────────┘         └──┘
typ     └──┘              └────────┘       └──┘
doc      └──┘               └────────┘          └──┘
 96  suffices splits id (f.map i) → ∃ s : multiset β, f.map i =
id            └────┘ └┘  └──┘          └──────┘  └──┘  
src           └────┘ └┘   └──┘           └──────┘    └──┘   
typ           └────┘ └┘  └──┘          └──────┘  └──┘  
doc           └────┘      └──┘            └──────┘     └──┘
 97    (C (f.map i).leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod,
id        └──┘  └───────────┘     └──┘              └────────┘       └──┘
src        └──┘   └───────────┘      └──┘               └────────┘         └──┘
typ       └──┘  └───────────┘     └──┘              └────────┘       └──┘
doc        └──┘   └───────────┘       └──┘               └────────┘          └──┘
 98  by rwa [splits_map_iff, leading_coeff_map i] at this,
id           └────────────┘  └───────────────┘ 
src     └───┘└────────────┘└┘└───────────────┘ └───────┘
typ     └───┘└────────────┘└┘└───────────────┘└───────┘
doc     └───┘              └┘                  └───────┘
txt     └───┘              └┘                  └───────┘
par     └───┘              └┘                  └───────┘
pid        └┘              └┘                  └──────┘
st     └──────────────────┘└───────────────────┘└──────┘
 99  is_noetherian_ring.irreducible_induction_on (f.map i)
id   └─────────────────────────────────────────┘  └──┘ 
src  └─────────────────────────────────────────┘   └──┘
typ  └─────────────────────────────────────────┘  └──┘ 
doc                                                └──┘
100    (λ _, ⟨{37}, by simp [is_ring_hom.map_zero i]⟩)
id                         └──────────────────┘ 
src                   └────┘└──────────────────┘ 
typ                  └────┘└──────────────────┘
doc                    └────┘└──────────────────┘ 
txt                    └────┘                     
par                    └────┘                     
pid                                             
st                    └────────────────────────────┘
101    (λ u hu _, ⟨0,
id         └┘ 
typ        └┘ 
102      by conv_lhs { rw eq_C_of_degree_eq_zero (is_unit_iff_degree_eq_zero.1 hu) };
id                        └────────────────────┘  └────────────────────────┘   └┘
src         └─────────┘└─┘└────────────────────┘ └────────────────────────┘└─┘  └┘
typ         └─────────┘└─┘└────────────────────┘ └────────────────────────┘└─┘└┘└┘
txt         └─────────┘└─┘                                                 └─┘  └┘
par         └─────────┘└─┘                                                 └─┘  └┘
pid                 └───┘                                                 └─┘  └─┘
st         └─────────┘└───────────────────────────────────────────────────────────┘└┘
103        simp [leading_coeff, nat_degree_eq_of_degree_eq_some (is_unit_iff_degree_eq_zero.1 hu)]⟩)
id               └───────────┘  └─────────────────────────────┘  └────────────────────────┘   └┘
src        └────┘└───────────┘└┘└─────────────────────────────┘ └────────────────────────┘└─┘  └┘
typ        └────┘└───────────┘└┘└─────────────────────────────┘ └────────────────────────┘└─┘└┘└┘
doc        └────┘└───────────┘└┘                                                          └─┘  └┘
txt        └────┘             └┘                                                          └─┘  └┘
par        └────┘             └┘                                                          └─┘  └┘
pid                         └┘                                                          └─┘  └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘
104    (λ f p hf0 hp ih hfs,
id          └─┘ └┘ └┘ └─┘
typ         └─┘ └┘ └┘ └─┘
105      have hpf0 : p * f ≠ 0, from mul_ne_zero hp.ne_zero hf0,
id                               └─────────┘ └┘└──────┘ └─┘
src                                └─────────┘   └──────┘
typ                              └─────────┘ └┘└──────┘ └─┘
st                  
106      let ⟨s, hs⟩ := ih (splits_of_splits_mul _ hpf0 hfs).2 in
id       └─┘           └┘  └──────────────────┘   └──┘ └─┘ 
src                         └──────────────────┘            
typ      └─┘           └┘  └──────────────────┘   └──┘ └─┘ 
107      ⟨-(p * norm_unit p).coeff 0 :: s,
id           └───────┘  └───┘    └┘
src           └───────┘   └───┘    └┘
typ          └───────┘  └───┘    └┘
doc                         └───┘    └┘
108        have hp1 : degree p = 1, from hfs.resolve_left hpf0 hp (by simp),
id                    └────┘           └─┘└───────────┘ └──┘ └┘
src                   └────┘               └───────────┘             └──┘
typ                   └────┘           └─┘└───────────┘ └──┘ └┘     └──┘
doc                   └────┘                                          └──┘
txt                                                                   └──┘
par                                                                   └──┘
st                                                                   └───┘
109        begin
st         └─────
110          rw [multiset.map_cons, multiset.prod_cons, leading_coeff_mul, C_mul, mul_assoc,
id               └───────────────┘  └────────────────┘  └───────────────┘  └───┘  └───────┘
src          └──┘└───────────────┘└┘└────────────────┘└┘└───────────────┘└┘└───┘└┘└───────┘└─
typ          └──┘└───────────────┘└┘└────────────────┘└┘└───────────────┘└┘└───┘└┘└───────┘└─
doc          └──┘                 └┘                  └┘                 └┘     └┘         └─
txt          └──┘                 └┘                  └┘                 └┘     └┘         └─
par          └──┘                 └┘                  └┘                 └┘     └┘         └─
pid            └┘                 └┘                  └┘                 └┘     └┘         └─
st   ────────────────────────────┘└──────────────────┘└─────────────────┘└─────┘└─────────┘└─
111            mul_left_comm (C f.leading_coeff), ← hs, ← mul_assoc, domain.mul_right_inj hf0],
id             └───────────┘   └─────────────┘     └┘    └───────┘  └──────────────────┘ └─┘
src  ─────────┘└───────────┘ └─────────────┘└───┘  └──┘└───────┘└┘└──────────────────┘   
typ  ─────────┘└───────────┘ └─────────────┘└───┘└┘└──┘└───────┘└┘└──────────────────┘└─┘
doc  ─────────┘              └─────────────┘└───┘  └──┘         └┘└──────────────────┘   
txt  ─────────┘                              └───┘  └──┘         └┘                       
par  ─────────┘                              └───┘  └──┘         └┘                       
pid  ─────────┘                              └───┘  └──┘         └┘                       
st   ──────────────────────────────────────────┘└────┘└───────────┘└────────────────────────┘└──
112          conv_lhs {rw eq_X_add_C_of_degree_eq_one hp1},
id                        └─────────────────────────┘ └─┘
src          └────────┘└─┘└─────────────────────────┘   
typ          └────────┘└─┘└─────────────────────────┘└─┘
txt          └────────┘└─┘                              
par          └────────┘└─┘                              
pid                  └──┘                              
st   ─────────────────┘└────────────────────────────────┘└┘
113          simp only [mul_add, coe_norm_unit hp.ne_zero, mul_comm p, coeff_neg,
id                      └─────┘  └───────────┘ └────────┘  └──────┘   └───────┘
src          └─────────┘└─────┘└┘└───────────┘└────────┘└┘└──────┘ └┘└───────┘└─
typ          └─────────┘└─────┘└┘└───────────┘└────────┘└┘└──────┘└┘└───────┘└─
doc          └─────────┘       └┘                       └┘         └┘         └─
txt          └─────────┘       └┘                       └┘         └┘         └─
par          └─────────┘       └┘                       └┘         └┘         └─
pid              └──┘└┘       └┘                       └┘         └┘         └─
st   ─────────────────────────────────────────────────────────────────────────────
114            C_neg, sub_eq_add_neg, neg_neg, coeff_C_mul, (mul_assoc _ _ _).symm, C_mul.symm,
id             └───┘  └────────────┘  └─────┘  └─────────┘   └───────┘
src  ─────────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────────┘└┘ └───────┘└────────────┘          └─
typ  ─────────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────────┘└┘ └───────┘└────────────┘└────────┘└─
doc  ─────────┘     └┘              └┘       └┘           └┘          └────────────┘          └─
txt  ─────────┘     └┘              └┘       └┘           └┘          └────────────┘          └─
par  ─────────┘     └┘              └┘       └┘           └┘          └────────────┘          └─
pid  ─────────┘     └┘              └┘       └┘           └┘          └────────────┘          └─
st   ───────────────────────────────────────────────────────────────────────────────────────────
115            mul_inv_cancel (show p.leading_coeff ≠ 0, from mt leading_coeff_eq_zero.1
id             └────────────┘       └─────────────┘          └┘ └───────────────────┘
src  ─────────┘└────────────┘     └─────────────┘└───────┘└┘└───────────────────┘└──
typ  ─────────┘└────────────┘     └─────────────┘└───────┘└┘└───────────────────┘└──
doc  ─────────┘                   └─────────────┘ └───────┘                       └──
txt  ─────────┘                                   └───────┘                       └──
par  ─────────┘                                   └───────┘                       └──
pid  ─────────┘                                   └───────┘                       └──
st   ────────────────────────────────────────────────────────────────────────────────────
116              hp.ne_zero), one_mul],
id               └────────┘   └─────┘
src  ───────────┘└────────┘└─┘└─────┘
typ  ───────────┘└────────┘└─┘└─────┘
doc  ───────────┘          └─┘       
txt  ───────────┘          └─┘       
par  ───────────┘          └─┘       
pid  ───────────┘          └─┘       
st   ────────────────────────────────┘└─
117        end⟩)
st   ────────┘
118  
119  section UFD
120  
121  local attribute [instance, priority 10] principal_ideal_domain.to_unique_factorization_domain
id                                           └───────────────────────────────────────────────────┘
src                                          └───────────────────────────────────────────────────┘
typ                                          └───────────────────────────────────────────────────┘
doc                                          └───────────────────────────────────────────────────┘
122  local infix ` ~ᵤ ` : 50 := associated
id                              └────────┘
src                             └────────┘
typ                             └────────┘
123  
124  open unique_factorization_domain associates
125  
126  lemma splits_of_exists_multiset {f : polynomial α} {s : multiset β}
id                                        └────────┘        └──────┘ 
src                                       └────────┘         └──────┘
typ                                       └────────┘        └──────┘ 
doc                                       └────────┘         └──────┘
127    (hs : f.map i = C (i f.leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod) :
id           └──┘      └────────────┘    └──┘              └────────┘       └──┘
src           └──┘         └────────────┘     └──┘               └────────┘         └──┘
typ          └──┘      └────────────┘    └──┘              └────────┘       └──┘
doc           └──┘          └────────────┘      └──┘               └────────┘          └──┘
128    splits i f :=
id     └────┘  
src    └────┘
typ    └────┘  
doc    └────┘
129  if hf0 : f = 0 then or.inl hf0
id   └┘                └────┘ └─┘
src  └┘                 └────┘
typ  └┘                └────┘ └─┘
130  else
131    or.inr $ λ p hp hdp,
id     └────┘     └┘ └─┘
src    └────┘
typ    └────┘     └┘ └─┘
132      have ht : multiset.rel associated
id                 └──────────┘ └────────┘
src                └──────────┘ └────────┘
typ                └──────────┘ └────────┘
doc                └──────────┘
133        (factors (f.map i)) (s.map (λ a : β, (X : polynomial β) - C a)) :=
id          └─────┘  └──┘     └──┘              └────────┘     
src         └─────┘   └──┘       └──┘               └────────┘     
typ         └─────┘  └──┘     └──┘              └────────┘     
doc                   └──┘       └──┘               └────────┘      
134      unique
id       └────┘
src      └────┘
typ      └────┘
135        (λ p hp, irreducible_factors (mt (map_eq_zero i).1 hf0) _ hp)
id             └┘  └─────────────────┘  └┘  └─────────┘    └─┘    └┘
src                 └─────────────────┘  └┘  └─────────┘   
typ            └┘  └─────────────────┘  └┘  └─────────┘    └─┘    └┘
136        (λ p, by simp [@eq_comm _ _ p, -sub_eq_add_neg,
id                        └─────┘     
src                 └────┘ └─────┘└───┘ └──────────────────
typ                └────┘ └─────┘└───┘└──────────────────
doc                 └────┘        └───┘ └──────────────────
txt                 └────┘        └───┘ └──────────────────
par                 └────┘        └───┘ └──────────────────
pid                             └───┘ └──────────────────
st                 └───────────────────────────────────────
137            irreducible_of_degree_eq_one (degree_X_sub_C _)] {contextual := tt})
id             └──────────────────────────┘  └────────────┘                    └┘
src  ─────────┘└──────────────────────────┘ └────────────┘└───┘ └────────────┘└┘
typ  ─────────┘└──────────────────────────┘ └────────────┘└───┘ └────────────┘└┘
doc  ─────────┘                                           └───┘ └────────────┘  
txt  ─────────┘                                           └───┘ └────────────┘  
par  ─────────┘                                           └───┘ └────────────┘  
pid  ─────────┘                                           └──┘ └────────────┘  
st   ────────────────────────────────────────────────────────────────────────────┘
138        (associated.symm $ calc _ ~ᵤ f.map i :
id          └─────────────┘             └──┘ 
src         └─────────────┘              └──┘
typ         └─────────────┘             └──┘ 
doc                                      └──┘
139          ⟨(units.map' C : units β →* units (polynomial β)) (units.mk0 (f.map i).leading_coeff
id             └────────┘    └───┘  └┘ └───┘  └────────┘     └───────┘  └──┘  └───────────┘
src            └────────┘    └───┘   └┘ └───┘  └────────┘      └───────┘   └──┘   └───────────┘
typ            └────────┘    └───┘  └┘ └───┘  └────────┘     └───────┘  └──┘  └───────────┘
doc            └────────┘            └┘        └────────┘      └───────┘   └──┘   └───────────┘
140              (mt leading_coeff_eq_zero.1 (mt (map_eq_zero i).1 hf0))),
id                └┘ └───────────────────┘   └┘  └─────────┘    └─┘
src               └┘ └───────────────────┘   └┘  └─────────┘   
typ               └┘ └───────────────────┘   └┘  └─────────┘    └─┘
141            by conv_rhs {rw [hs, ← leading_coeff_map i, mul_comm]}; refl⟩
id                              └┘    └───────────────┘   └──────┘
src               └────────┘└──┘  └──┘└───────────────┘ └┘└──────┘  └──┘
typ               └────────┘└──┘└┘└──┘└───────────────┘└┘└──────┘  └──┘
doc                                                                    └──┘
txt               └────────┘└──┘  └──┘                  └┘          └──┘
par               └────────┘└──┘  └──┘                  └┘          └──┘
pid                       └───┘  └──┘                  └┘        └┘
st               └─────────┘└────┘└─────────────────────┘└────────┘ └┘└───┘
142          ... ~ᵤ _ : associated.symm (unique_factorization_domain.factors_prod (by simpa using hf0))),
id                      └─────────────┘  └──────────────────────────────────────┘                 └─┘
src                     └─────────────┘  └──────────────────────────────────────┘     └──────────┘
typ                     └─────────────┘  └──────────────────────────────────────┘     └──────────┘└─┘
doc                                                                                   └──────────┘
txt                                                                                   └──────────┘
par                                                                                   └──────────┘
pid                                                                                        └────┘
st                                                                                   └──────────────┘
143    let ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd (by simpa) hp hdp in
id     └─┘     └┘          └───────────────────────┘            └┘ └─┘
src                        └───────────────────────┘     └───┘
typ    └─┘     └┘          └───────────────────────┘     └───┘  └┘ └─┘
doc                                                      └───┘
txt                                                      └───┘
par                                                      └───┘
st                                                      └────┘
144    let ⟨q', hq', hqq'⟩ := multiset.exists_mem_of_rel_of_mem ht hq in
id     └─┘      └─┘           └───────────────────────────────┘ └┘
src                           └───────────────────────────────┘
typ    └─┘      └─┘           └───────────────────────────────┘ └┘
145    let ⟨a, ha⟩ := multiset.mem_map.1 hq' in
id     └─┘            └──────────────┘
src                   └──────────────┘
typ    └─┘            └──────────────┘
146    by rw [← degree_X_sub_C a, ha.2];
id              └────────────┘   └┘
src       └────┘└────────────┘ └┘  └─┘
typ       └────┘└────────────┘└┘└┘└─┘
doc       └────┘               └┘  └─┘
txt       └────┘               └┘  └─┘
par       └────┘               └┘  └─┘
pid         └──┘               └┘  └─┘
st       └─────────────────────┘└──┘└─┘└─
147      exact degree_eq_degree_of_associated (hpq.trans hqq')
id             └────────────────────────────┘  └───────┘ └──┘
src      └────┘└────────────────────────────┘ └───────┘    └─
typ      └────┘└────────────────────────────┘ └───────┘└──┘└─
doc      └────┘                                            └─
txt      └────┘                                            └─
par      └────┘                                            └─
pid                                                       
st   ──────────────────────────────────────────────────────────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  lemma splits_of_splits_id {f : polynomial α} : splits id f → splits i f :=
id                                  └────────┘     └────┘ └┘    └────┘  
src                                 └────────┘      └────┘ └┘     └────┘
typ                                 └────────┘     └────┘ └┘    └────┘  
doc                                 └────────┘      └────┘        └────┘
150  unique_factorization_domain.induction_on_prime f (λ _, splits_zero _)
id   └────────────────────────────────────────────┘       └─────────┘
src  └────────────────────────────────────────────┘         └─────────┘
typ  └────────────────────────────────────────────┘       └─────────┘
151    (λ _ hu _, splits_of_degree_le_one _
id         └┘   └─────────────────────┘
src               └─────────────────────┘
typ        └┘   └─────────────────────┘
152      ((is_unit_iff_degree_eq_zero.1 hu).symm ▸ dec_trivial))
id         └────────────────────────┘  └┘ └──┘   └─────────┘
src        └────────────────────────┘     └──┘   └─────────┘
typ        └────────────────────────┘  └┘ └──┘   └─────────┘
doc                                                └─────────┘
153    (λ a p ha0 hp ih hfi, splits_mul _
id          └─┘ └┘ └┘ └─┘  └────────┘
src                          └────────┘
typ         └─┘ └┘ └┘ └─┘  └────────┘
154      (splits_of_degree_eq_one _
id        └─────────────────────┘
src       └─────────────────────┘
typ       └─────────────────────┘
155        ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.resolve_left
id           └──────────────────┘    └─────────┘ └┘  └─┘  └─┘  └──────────┘
src          └──────────────────┘    └─────────┘               └──────────┘
typ          └──────────────────┘    └─────────┘ └┘  └─┘  └─┘  └──────────┘
156          hp.1 (irreducible_of_prime hp) (by rw map_id)))
id           └┘   └──────────────────┘ └┘         └────┘
src               └──────────────────┘         └─┘└────┘
typ          └┘   └──────────────────┘ └┘      └─┘└────┘
doc                                             └─┘
txt                                             └─┘
par                                             └─┘
pid                                               
st                                             └────────┘
157      (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2))
id        └┘  └──────────────────┘    └─────────┘ └┘  └─┘  └─┘ 
src           └──────────────────┘    └─────────┘              
typ       └┘  └──────────────────┘    └─────────┘ └┘  └─┘  └─┘ 
158  
159  end UFD
160  
161  lemma splits_iff_exists_multiset {f : polynomial α} : splits i f ↔
id                                         └────────┘     └────┘   
src                                        └────────┘      └────┘     
typ                                        └────────┘     └────┘   
doc                                        └────────┘      └────┘
162    ∃ (s : multiset β), f.map i = C (i f.leading_coeff) *
id           └──────┘   └──┘      └────────────┘  
src          └──────┘     └──┘         └────────────┘  
typ          └──────┘   └──┘      └────────────┘  
doc           └──────┘      └──┘          └────────────┘
163    (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
id      └──┘              └────────┘       └──┘
src      └──┘               └────────┘         └──┘
typ     └──┘              └────────┘       └──┘
doc      └──┘               └────────┘          └──┘
164  ⟨exists_multiset_of_splits i, λ ⟨s, hs⟩, splits_of_exists_multiset i hs⟩
id    └───────────────────────┘        └┘   └───────────────────────┘ 
src   └───────────────────────┘               └───────────────────────┘
typ   └───────────────────────┘        └┘   └───────────────────────┘ 
165  
166  lemma splits_comp_of_splits (j : β → γ) [is_ring_hom j] {f : polynomial α}
id                                          └─────────┘        └────────┘ 
src                                           └─────────┘         └────────┘
typ                                         └─────────┘        └────────┘ 
doc                                           └─────────┘         └────────┘
167    (h : splits i f) : splits (λ x, j (i x)) f :=
id          └────┘      └────┘            
src         └────┘        └────┘
typ         └────┘      └────┘            
doc         └────┘        └────┘
168  begin
st   └─────
169    change i with (λ x, id (i x)) at h,
id                        └┘  
src    └─────┘ └────┘  └──┘└┘   └─────┘
typ    └─────┘└────┘  └──┘└┘  └─────┘
doc    └─────┘ └────┘  └──┘     └─────┘
txt    └─────┘ └────┘  └──┘     └─────┘
par    └─────┘ └────┘  └──┘     └─────┘
pid           └────┘  └──┘     └┘└───┘
st   ───────────────────────────────────┘└─
170    rw [← splits_map_iff],
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid      └──┘              
st   ─────────────────────┘└──
171    rw [← splits_map_iff i id] at h,
id           └────────────┘  └┘
src    └────┘└────────────┘ └┘└────┘
typ    └────┘└────────────┘└┘└────┘
doc    └────┘                 └────┘
txt    └────┘                 └────┘
par    └────┘                 └────┘
pid      └──┘                 └───┘
st   ──────────────────────────┘└───┘└─
172    exact splits_of_splits_id _ h
id           └─────────────────┘   
src    └────┘└─────────────────┘└─┘ 
typ    └────┘└─────────────────┘└─┘
doc    └────┘                   └─┘ 
txt    └────┘                   └─┘ 
par    └────┘                   └─┘ 
pid                            └─┘ 
st   ───────────────────────────────┘
173  end
st   └─┘
174  
175  end splits
176  
177  end polynomial